T:Type, l1, l2, l3:(T List). fseg(T;l1;l2)  fseg(T;l1;l3 @ l2) 

latex

ProofTree

Definitions	as @ bs, fseg(T;L1;L2), x:A. B(x), A List, [], i  j , A  B, [car / cdr], SQType(T), {T}, s ~ t, , S  T, Top, x:A.B(x), Void, {x:A| B(x)} , ||as||, , P  Q, P & Q, x:A  B(x), P  Q, P  Q, Type, , type List, x:A. B(x), x:AB(x), s = t, t  T
Lemmas	append wf, append assoc, rev implies wf, iff wf, member wf, top wf, length wf nat, nat wf, guard wf, cons one one, non neg length